\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it is\_req}$, ${\it is\_ack}$:(E$\rightarrow\mathbb{P}$), ${\it awaiting}$, ${\it owes\_ack}$:(Id$\rightarrow$Id$\rightarrow$Id).
\\[0ex](${\it ff}$.C $\subseteq$r Id)
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:${\it ff}$.C. @$i$(${\it awaiting}$($i$,$j$):$\mathbb{B}$) \& @$i$(${\it owes\_ack}$($i$,$j$):$\mathbb{B}$))
\\[0ex]$\Rightarrow$ ($\forall$$i$:${\it ff}$.C, $e$:E. (${\it ff}$.R($i$,$e$)) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec(${\it is\_req}$($e$)) \& Dec(${\it is\_ack}$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.S($i$,$j$,$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:${\it ff}$.C, $e$:E. (${\it ff}$.S($i$,$j$,$e$)) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]$\Rightarrow$ plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;${\it is\_req}$;${\it is\_ack}$;${\it awaiting}$;${\it owes\_ack}$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$:E.\+
\\[0ex][$e$: ${\it rcvr}$ $--$${\it is\_ack}$$\rightarrow$ ${\it sndr}$] $\Rightarrow$ ($\exists$$x$:E. (($x$ $<$loc $e$) \& [$x$: ${\it rcvr}$ $\leftarrow$${\it is\_req}$$--$ ${\it sndr}$])))
\-
\end{tabbing}